package arlab.formulae
import arlab.formulae.transformations._


/**
 * Created by IntelliJ IDEA.
 * User: Eve
 * Date: 23.02.12
 * Time: 15:54
 * To change this template use File | Settings | File Templates.
 */

// Kripke Struktur ist ein 5- Tupel aus: Zuständen, Startzuständen, Transitions-Relation,Zustandsbeschriftung und Zustandsinhalt
case class Kripke(states: List[Int], transitions:List[(Int,  Int)], initStates: List[Int], labelFunc: Map[Int,  List[BooleanVariable]],labels: List[BooleanVariable] ) extends TransitionSystem  {

  def init(step:Int):Formula={
    Transformations.simplify(initStates.foldLeft(False:Formula) {(total, n) => Or(total, code(n))}).renameAllVariables(step)
   }
  
  def code(i:Int): Formula =  labelFunc.get(i) match {
    case Some(a) => code_helper(a)
    case None => code_helper(List())
  }

  def code_helper(x:List[BooleanVariable]):Formula ={
    val ls = labels.diff(x)
    And(ls.map(Not(_)).foldLeft(True:Formula){(total, n) => And(total,n)},
      x.foldLeft(True:Formula){(total, n) => And(total,n)})
  }

  def step(i:Int,  j:Int):Formula = {
    Transformations.simplify(transitions.foldLeft(False:Formula) {(total, n) => Or(And(code(n._1).renameAllVariables(i), code(n._2).renameAllVariables(j)) , total)})
  }
  

}
